es:ES, ff:FIFO, p:(E), e:E, sndr, rcvr:ff.C.
(e:E. Dec(p(e)))  (e:E. Dec(ff.S(sndr,rcvr,e)))  Dec([e: sndr p rcvr]) 

latex

Definitions	x:A. B(x), , P  Q, x(s), t  T, [e: i p j], P & Q, A c B
Lemmas	es-E wf, decidable wf, fifoS wf, fifoC wf, FIFO wf, event system wf, decidable cand